the_w:World, e, e':E. e = e'   

latex

Definitions	E, p = q, p  q, a = b, i=j, A, b, isnull(a), 1of(t), a(i;t), 2of(t), , Id, x. t(x), x:A. B(x), t  T, World
Lemmas	world wf, pi2 wf, w-a wf, pi1 wf, w-isnull wf, assert wf, not wf, nat wf, Id wf, eq int wf, eq id wf, band wf